package interfaces.gestores;

import interfaces.IProducto;
import tdg.contract.semanticAnnotations.Model;
import tdg.contract.semanticAnnotations.Query;
import tdg.contract.semanticAnnotations.Pre;
import tdg.contract.semanticAnnotations.Pos;

public interface IGestorProductosWithModel extends IGestorProductosModel,
		IGestorProductos {
	
	@Pre ({"p!=null #NullPointerException", "!estaProducto(p)"})
	@Pos ({"estaProducto(p)"})
	public void altaProducto(IProducto p);
	
	@Pre ({"p!=null #NullPointerException", "estaProducto(p)"})
	@Pos ({"!estaProducto(p)"})
	public void bajaProducto(IProducto p);
	
	@Pre ({"p1!=null && p2!=null #NullPointerException", "estaProducto(p1) && p1.getCodigo()==p2.getCodigo()"})
	@Pos ({"!estaProducto(p1) && estaProducto(p2)"})
	public void modificacionProducto(IProducto p1, IProducto p2);

}
